\begin{tabbing}
ESAxioms\=\{i:l\}\+
\\[0ex](\=$E$;\+
\\[0ex]$T$;
\\[0ex]$M$;
\\[0ex]${\it loc}$;
\\[0ex]${\it kind}$;
\\[0ex]${\it val}$;
\\[0ex]${\it when}$;
\\[0ex]${\it after}$;
\\[0ex]${\it time}$;
\\[0ex]${\it sends}$;
\\[0ex]${\it sender}$;
\\[0ex]${\it index}$;
\\[0ex]${\it first}$;
\\[0ex]${\it pred}$;
\\[0ex]${\it causl}$)
\-\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(\=$\forall$$e$:$E$, ${\it e'}$:$E$.\+\+
\\[0ex](${\it loc}$($e$) = ${\it loc}$(${\it e'}$) $\in$ Id) $\Rightarrow$ ((${\it causl}$($e$,${\it e'}$)) $\vee$ ($e$ = ${\it e'}$ $\in$ $E$) $\vee$ (${\it causl}$(${\it e'}$,$e$))))
\-\\[0ex]\& ($\forall$$e$:$E$. ($\uparrow$(${\it first}$($e$))) $\Leftarrow\!\Rightarrow$ ($\forall$${\it e'}$:$E$. (${\it loc}$(${\it e'}$) = ${\it loc}$($e$) $\in$ Id) $\Rightarrow$ ($\neg$(${\it causl}$(${\it e'}$,$e$)))))
\\[0ex]\& (\=$\forall$$e$:$E$.\+
\\[0ex]($\neg$($\uparrow$(${\it first}$($e$))))
\\[0ex]$\Rightarrow$ \=(${\it loc}$(${\it pred}$($e$)) = ${\it loc}$($e$) $\in$ Id \& ${\it causl}$(${\it pred}$($e$),$e$)\+
\\[0ex]\& ($\forall$${\it e'}$:$E$. (${\it loc}$(${\it e'}$) = ${\it loc}$($e$) $\in$ Id) $\Rightarrow$ ($\neg$(${\it causl}$(${\it pred}$($e$),${\it e'}$) \& ${\it causl}$(${\it e'}$,$e$))))))
\-\-\\[0ex]\& (\=$\forall$$e$:$E$.\+
\\[0ex]($\neg$($\uparrow$(${\it first}$($e$))))
\\[0ex]$\Rightarrow$ \=($\forall$$x$:Id, $t$:$\mathbb{Q}$.\+
\\[0ex]${\it when}$($x$,$e$,$t$)
\\[0ex]=
\\[0ex]${\it after}$($x$,${\it pred}$($e$),$t$ + ((${\it time}$($e$)) {-} (${\it time}$(${\it pred}$($e$)))))
\\[0ex]$\in$ $T$(${\it loc}$($e$),$x$)))
\-\-\\[0ex]\& Trans($E$;$e$,${\it e'}$.${\it causl}$($e$,${\it e'}$))
\\[0ex]\& strongwellfounded($E$; $e$,${\it e'}$.(${\it causl}$($e$,${\it e'}$)))
\\[0ex]\& (\=$\forall$$e$:$E$.\+
\\[0ex]($\uparrow$isrcv(${\it kind}$($e$)))
\\[0ex]$\Rightarrow$ (\=(${\it sends}$(lnk(${\it kind}$($e$)),${\it sender}$($e$)))[(${\it index}$($e$))]\+
\\[0ex]=
\\[0ex]msg(lnk(${\it kind}$($e$));tag(${\it kind}$($e$));${\it val}$($e$))
\\[0ex]$\in$ Msg($M$)))
\-\-\\[0ex]\& ($\forall$$e$:$E$. ($\uparrow$isrcv(${\it kind}$($e$))) $\Rightarrow$ (${\it causl}$(${\it sender}$($e$),$e$)))
\\[0ex]\& (\=$\forall$$e$:$E$, ${\it e'}$:$E$.\+
\\[0ex](${\it causl}$($e$,${\it e'}$))
\\[0ex]$\Rightarrow$ \=((($\neg$($\uparrow$(${\it first}$(${\it e'}$)))) c$\wedge$ ((${\it causl}$($e$,${\it pred}$(${\it e'}$))) $\vee$ ($e$ = ${\it pred}$(${\it e'}$) $\in$ $E$)))\+
\\[0ex]$\vee$ (($\uparrow$isrcv(${\it kind}$(${\it e'}$))) c$\wedge$ ((${\it causl}$($e$,${\it sender}$(${\it e'}$))) $\vee$ ($e$ = ${\it sender}$(${\it e'}$) $\in$ $E$)))))
\-\-\\[0ex]\& ($\forall$$e$:$E$. ($\uparrow$isrcv(${\it kind}$($e$))) $\Rightarrow$ (${\it loc}$($e$) = destination(lnk(${\it kind}$($e$))) $\in$ Id))
\\[0ex]\& (\=$\forall$$e$:$E$, $l$:IdLnk.\+
\\[0ex]($\neg$(${\it loc}$($e$) = source($l$) $\in$ Id)) $\Rightarrow$ (${\it sends}$($l$,$e$) = [] $\in$ (Msg\_sub($l$;$M$) List)))
\-\\[0ex]\& (\=$\forall$$e$:$E$, ${\it e'}$:$E$.\+
\\[0ex]($\uparrow$isrcv(${\it kind}$($e$)))
\\[0ex]$\Rightarrow$ ($\uparrow$isrcv(${\it kind}$(${\it e'}$)))
\\[0ex]$\Rightarrow$ (lnk(${\it kind}$($e$)) = lnk(${\it kind}$(${\it e'}$)) $\in$ IdLnk)
\\[0ex]$\Rightarrow$ \=((${\it causl}$($e$,${\it e'}$))\+
\\[0ex]$\Leftarrow\!\Rightarrow$ \=((${\it causl}$(${\it sender}$($e$),${\it sender}$(${\it e'}$)))\+
\\[0ex]$\vee$ (${\it sender}$($e$) = ${\it sender}$(${\it e'}$) $\in$ $E$ \& ((${\it index}$($e$)) $<$ (${\it index}$(${\it e'}$)))))))
\-\-\-\\[0ex]\& (\=$\forall$$e$:$E$, $l$:IdLnk, $n$:\{0..$\parallel$${\it sends}$($l$,$e$)$\parallel^{-}$\}.\+
\\[0ex]$\exists$\=${\it e'}$:$E$\+
\\[0ex](($\uparrow$isrcv(${\it kind}$(${\it e'}$)))
\\[0ex]c$\wedge$ (lnk(${\it kind}$(${\it e'}$)) = $l$ $\in$ IdLnk \& ${\it sender}$(${\it e'}$) = $e$ $\in$ $E$ \& ${\it index}$(${\it e'}$) = $n$ $\in$ $\mathbb{Z}$)))
\-\-\-
\end{tabbing}